\documentclass[DaoFP]{subfiles}
\begin{document}
\setcounter{chapter}{4}

\chapter{Product Types}

We can use sum types to enumerate possible values of a given type, but the encoding can be wasteful. We needed ten constructors just to encode numbers between zero and nine.
\begin{haskell}
data Digit = Zero | One | Two | Three | ... | Nine
\end{haskell}
But if we combine two digits into a single data structure, a two-digit decimal number, we'll be able to encode a hundred numbers. Or, as Lao Tzu would say, with just four digits you can encode ten thousand numbers.

A data type that combines two types in this manner is called a product, or a \index{cartesian product}\emph{cartesian} product. Its defining quality is the elimination rule: there are two arrows coming from $a \times b$; one called ``$\text{fst}$'' goes to $a$, and another called ``$\text{snd}$'' goes to $b$. They are called (cartesian) \index{cartesian projections}\emph{projections}. They let us retrieve $a$ and $b$ from the product $a \times b$.

\[
 \begin{tikzcd}
& a \times b
 \arrow[dl,  "\text{fst}"]
 \arrow[dr,   "\text{snd}"']
\\
a && b
 \end{tikzcd}
\]

Suppose that somebody gave you an element of a product, that is an arrow $h$ from the terminal object $1$ to $a \times b$. You can easily retrieve a pair of elements, just by using composition: an element of $a$ given by 
\[x = \text{fst} \circ h \]
and an element of $b$ given by
\[y = \text{snd} \circ h \]

\[
 \begin{tikzcd}
 & 1
\arrow[d, dashed, "h"]
 \arrow[ddl, bend right, "x"']
 \arrow[ddr, bend left, "y"]
\\
&a \times b
 \arrow[dl,  "\text{fst}"]
 \arrow[dr,   "\text{snd}"']
\\
a && b
 \end{tikzcd}
\]

In fact, given an arrow from an arbitrary object $c$ to $a \times b$, we can define, by composition, a pair of arrows $f \colon c \to a$ and $g \colon c \to b$

\[
 \begin{tikzcd}
 & c
\arrow[d, dashed, "h"]
 \arrow[ddl, bend right, "f"']
 \arrow[ddr, bend left, "g"]
\\
&a \times b
 \arrow[dl,  "\text{fst}"]
  \arrow[dr,   "\text{snd}"']
\\
a && b
 \end{tikzcd}
\]

As we did before with the sum type, we can turn this idea around, and use this diagram to \emph{define} the product type: We impose the condition that a pair of functions $f$ and $g$ be in one-to-one correspondence with a \index{mapping in}\emph{mapping in} from $c$ to $a \times b$. This is the \emph{introduction} rule for the product.

In particular, the mapping out of the terminal object is used in Haskell to define a product type. Given two elements, \hask{a :: A} and \hask{b :: B}, we construct the product 

\begin{haskell}
(a, b) :: (A, B)
\end{haskell}
The built-in syntax for products is just that: a pair of parentheses and a comma in between. It works both for defining the product of two types \hask{(A, B)} and the data constructor \hask{(a, b)} that takes two elements and pairs them together. 

We should never lose sight of the purpose of programming: to decompose complex problems into a series of simpler ones. We see it again in the definition of the product. Whenever we have to construct a mapping \emph{into} the product, we decompose it into two smaller tasks of constructing a pair of functions, each mapping into one of the components of the product. This is as simple as saying that, in order to implement a function that returns a pair of values, it's enough to implement two functions, each returning one of the elements of the pair.

\subsection{Logic}

In logic, a product type corresponds to logical conjunction. In order to prove $A \times B$ ($A$ and $B$), you need to provide the proofs of \emph{both} $A$ and $B$. These are the arrows targeting $A$ and $B$. The elimination rule says that if you have a proof of $A \times B$, then you automatically get the proof of $A$ (through $\text{fst}$) and the proof of $B$ (through $\text{snd}$).

\subsection{Tuples and Records}

As Lao Tzu would say, a product of ten thousand objects is just an object with ten thousand projections. 

We can form arbitrary products in Haskell using the tuple notation. For instance, a product of three types is written as \hask{(A, B, C)}. A term of this type can be constructed from three elements: \hask{(a, b, c)}. 

In what mathematicians call ``abuse of notation'', a product of zero types is written as \hask{()}, an empty tuple, which happens to be the same as the terminal object, or unit type. This is because the product behaves very much like multiplication of numbers, with the terminal object playing the role of one.

In Haskell, rather than defining separate projections for all tuples, we use the pattern-matching syntax. For instance, to extract the third component from a triple we would write

\begin{haskell}
thrd :: (a, b, c) -> c
thrd (_, _, c) = c
\end{haskell}
We use wildcards for the components that we want to ignore.

Lao Tzu said that ``Naming is the origin of all particular things.'' In programming, keeping track of the meaning of the components of a particular tuple is difficult without giving them names. Record syntax allows us to give names to projections. This is the definition of a product written in record style:
\begin{haskell}
data Product a b = Pair { fst :: a, snd :: b }
\end{haskell}
\hask{Pair} is the data constructor and \hask{fst} and \hask{snd} are the projections. 

This is how it could be used to declare and initialize a particular pair:
\begin{haskell}
ic :: Product Int Char
ic = Pair 10 'A'
\end{haskell}

\section{Cartesian Category}

In Haskell, we can define a product of any two types. A category in which all products exist, and the terminal object exists, is called \emph{cartesian}. 

\subsection{Tuple Arithmetic}

The identities satisfied by the product can be derived using the mapping-in property. For instance, to show that $a \times b \cong b \times a$ consider the following two diagrams:

\[
 \begin{tikzcd}
 &x
 \arrow[d, dashed, "h"]
 \arrow[ddl, bend right, "f"']
 \arrow[ddr, bend left, "g"]
 \\
 & a \times b
  \arrow[dl,  "\text{fst}"]
 \arrow[dr,   "\text{snd}"']
 \\
a && b
 \end{tikzcd}
 \qquad
 \begin{tikzcd}
 &x
 \arrow[d, dashed, "h'"]
 \arrow[ddl, bend right, "g"']
 \arrow[ddr, bend left, "f"]
 \\
 & b \times a
  \arrow[dl,  "\text{fst}"]
 \arrow[dr,   "\text{snd}"']
\\
b && a
  \end{tikzcd}
\]

They show that, for any object $x$ the arrows to $a \times b$ are in one-to-one correspondence with arrows to $b \times a$. This is because each of these arrows is determined by the same pair $f$ and $g$. 

You can check that the naturality condition is satisfied because, when you shift the perspective using $k \colon x' \to x$, all arrows originating in $x$ are shifted by pre-composition $(- \circ k)$.

In Haskell, this isomorphism can be implemented as a function which is its own inverse:
\begin{haskell}
swap :: (a, b) -> (b, a)
swap x = (snd x, fst x)
\end{haskell}
Here's the same function written using pattern matching:
\begin{haskell}
swap (x, y) = (y, x)
\end{haskell}

It's important to keep in mind that the product is symmetric only ``up to isomorphism.'' It doesn't mean that swapping the order of pairs won't change the behavior of a program. Symmetry means that the information content of a swapped pair is the same, but access to it needs to be modified.

The terminal object is the unit of the product, $1 \times a \cong a$. The arrow that witnesses the isomorphism between $1 \times a$ and $a$ is called the \emph{left unitor}:
\[ \lambda \colon 1 \times a \to a \]
It can be implemented as $\lambda = \text{snd}$. Its inverse $\lambda^{-1}$ is defined as the unique arrow in the following diagram:
\[
 \begin{tikzcd}
 &a
 \arrow[d, dashed, "\lambda^{-1}"]
 \arrow[ddl, bend right, "!"']
 \arrow[ddr, bend left, "\text{id}"]
 \\
 & 1 \times a
  \arrow[dl,  "\text{fst}"]
 \arrow[dr,   "\text{snd}"']
 \\
1 && a
 \end{tikzcd}
 \]
The arrow from $a$ to $1$ is called \index{!}$!$ (pronounced, \emph{bang}). This indeed shows that 
\[\text{snd} \circ \lambda^{-1} = \text{id} \] 
We still have to prove that $\lambda^{-1}$ is the left inverse of $\text{snd}$. Consider the following diagram:
\[
 \begin{tikzcd}
 &1 \times a
 \arrow[d, dashed, "h"]
 \arrow[ddl, bend right, "!"']
 \arrow[ddr, bend left, "\text{snd}"]
 \\
 & 1 \times a
  \arrow[dl,  "\text{fst}"]
 \arrow[dr,   "\text{snd}"']
 \\
1 && a
 \end{tikzcd}
 \]
 It obviously commutes for $h = id$. It also commutes for $h = \lambda^{-1}  \circ  \text{snd}$, because we have:
 \[  \text{snd} \circ \lambda^{-1}  \circ  \text{snd} = \text{snd} \]
 Since $h$ is supposed to be unique, we conclude that:
\[ \lambda^{-1}  \circ  \text{snd} = id \]
This kind of reasoning with universal constructions is pretty standard.

Here are some other isomorphisms written in Haskell (without proofs of having the inverse). This is associativity:
\begin{haskell}
assoc :: ((a, b), c) -> (a, (b, c))
assoc ((a, b), c) = (a, (b, c))
\end{haskell}
And this is the right unit
\begin{haskell}
runit :: (a, ()) -> a
runit (a, _) = a
\end{haskell}

These two functions correspond to the \index{associator}\emph{associator}
\[ \alpha \colon (a \times b) \times c \to a \times (b \times c) \]
and the \index{unitor}\emph{right unitor}:
\[ \rho \colon a \times 1 \to a \]

\begin{exercise}
Show that the bijection in the proof of left unit is natural. Hint, change focus using an arrow $g \colon a \to b$.
\end{exercise}

\begin{exercise}
Construct an arrow 
\[ h \colon b + a \times b \to (1 + a) \times b \]
Is this arrow unique?

Hint: It's a mapping into a product, so it's given by a pair of arrow. These arrows, in turn, map out of a sum, so each is given by a pair of arrows. 

Hint: The mapping $b \to 1 + a$ is given by $(\text{Left} \, \circ \, !)$
\end{exercise}

\begin{exercise}
Redo the previous exercise, this time treating $h$ as a mapping \emph{out} of a sum. 
\end{exercise}

\begin{exercise}
Implement a Haskell function \hask{maybeAB :: Either b (a, b) -> (Maybe a, b)}. Is this function uniquely defined by its type signature or is there some leeway?
\end{exercise}

\subsection{Functoriality}

Suppose that we have arrows that map $a$ and $b$ to some $a'$ and $b'$:
\begin{align*}
f &\colon a \to a' \\
g &\colon b \to b'
\end{align*}
The composition of these arrows with the projections $\text{fst}$ and $\text{snd}$, respectively, can be used to define the mapping $h$ between the products:

\[
 \begin{tikzcd}
 & a \times b
\arrow[d, dashed, "h"]
 \arrow[dl,  "\text{fst}"']
 \arrow[dr,   "\text{snd}"]
\\
a
\arrow[d, "f"']
&a' \times b'
 \arrow[dl,  "\text{fst}"]
  \arrow[dr,   "\text{snd}"']
& b
\arrow[d, "g"]
\\
a' && b'
 \end{tikzcd}
\]
The shorthand notation for this diagram is:
\[ a \times b \xrightarrow{f \times g} a' \times b' \]

This property of the product is called \emph{functoriality}. You can imagine it as allowing you to transform the two objects \emph{inside} the product to get the new product. We also say that functoriality lets us \index{lifting}\emph{lift} a pair of arrows in order to operate on products.

\section{Duality}

When a child sees an arrow, it knows which end points at the source, and which points at the target
\[a \to b \]
But maybe this is just a preconception. Would the Universe be very different if we called $b$ the source and $a$ the target? 

We would still be able to compose this arrow with this one
\[b \to c\]
whose ``target'' $b$ is the same as the same as the ``source'' of $a \to b$, and the result would still be an arrow 
\[a \to c\]
 only now we would say that it goes from $c$ to $a$.

In this dual Universe, the object that we call ``initial'' would be called ``terminal,'' because it's the ``target'' of unique arrows coming from all objects. Conversely, the terminal object would be called initial.

Now consider this diagram that we used to define the sum object:
\[
 \begin{tikzcd}
 a
 \arrow[dr,  bend left, "\text{Left}"']
 \arrow[ddr, bend right, "f"']
 && b
 \arrow[dl, bend right, "\text{Right}"]
 \arrow[ddl, bend left, "g"]
 \\
&a + b
\arrow[d, dashed, "h"]
\\
& c
 \end{tikzcd}
\]
In the new interpretation, the arrow $h$ would go ``from'' an arbitrary object $c$ ``to'' the object we call $a + b$. This arrow is uniquely defined by a pair of arrows $(f, g)$ whose ``source'' is $c$. If we rename $\text{Left}$ to $\text{fst}$ and $\text{Right}$ to $\text{snd}$, we will get  the defining diagram for a product. 

A product is the sum with arrows reversed. 

Conversely, a sum is the product with arrows reversed. 

\medskip

Every construction in category theory has its dual.

\medskip

If the direction of arrows is just a matter of interpretation, then what makes sum types so different from product types, in programming? The difference goes back to one assumption we made at the start: There are no incoming arrows to the initial object (other than the identity arrow). This is in contrast with the terminal object having lots of outgoing arrows, arrows that we used to define (global) elements. In fact, we assume that every object of interest has elements, and the ones that don't are isomorphic to \hask{Void}. 

We'll see an even deeper difference when we talk about function types.

\section{Monoidal Category}

We have seen that the product satisfies these simple rules:
\begin{align*}
1 \times a &\cong a
\\
a \times b &\cong b \times a
\\
(a \times b) \times c &\cong a \times (b \times c)
\end{align*}
and is functorial. 

A category in which an operation with these properties is defined is called \emph{symmetric monoidal}\footnote{Strictly speaking, a product of two objects is defined up to isomorphism, whereas the product in a monoidal category must be defined on the nose. But we can get a monoidal category by making a choice of a product}. We've seen a similar structure before, when working with sums and the initial object. 

A category can have multiple monoidal structures at the same time. When you don't want to name your monoidal structure, you replace the plus sign or the product sign with a tensor sign, and the neutral element with the letter $I$. The rules of a symmetric monoidal category can then be written as:
\begin{align*}
I \otimes a &\cong a
\\
a \otimes b &\cong b \otimes a
\\
(a \otimes b) \otimes c &\cong a \otimes (b \otimes c)
\end{align*}

These isomorphisms are often written as families of invertible arrows called \index{associator}associators and \index{unitor}unitors. If the monoidal category is not symmetric, there is a separate left and right unitor.
\begin{align*}
\alpha &\colon (a \otimes b) \otimes c \to a \otimes (b \otimes c)
\\
 \lambda &\colon I \otimes a \to a
 \\
 \rho &\colon a \otimes I \to a
\end{align*}
The symmetry is witnessed by:
\[ \gamma \colon a \otimes b \to b \otimes a \]
Functoriality lets us \emph{lift} a pair of arrows:
\begin{align*} 
f &\colon a \to a' \\
g &\colon b \to b'
\end{align*}
 to operate on tensor products:
\[ a \otimes b \xrightarrow{f \otimes g} a' \otimes b' \]

If we think of morphisms as actions, their tensor product corresponds to performing two actions in parallel. Contrast this with the serial composition of morphisms, which suggests their temporal ordering.

You may think of a tensor product as the lowest common denominator of product and sum. It still has an introduction rule, which requires both objects $a$ and $b$; but it has no elimination rule. Once created, a tensor product ``forgets'' how it was created. Unlike a cartesian product, it has no projections. 

Some interesting examples of tensor products are not even symmetric. 

\subsection{Monoids}

Monoids are very simple structures equipped with a binary operation and a unit. Natural numbers with addition and zero form a monoid. So do natural numbers with multiplication and one. 

The intuition is that a monoid lets you combine two things to get another thing. There is also one special thing, such that combining it with anything else gives back the same thing. That's the unit. And the combining must be associative. 

What's not assumed is that the combining is symmetric, or that there is an inverse element.

The rules that define a monoid are reminiscent of the rules of a category. The difference is that, in a monoid, any two things are composable, whereas in a category this is usually not the case: You can only compose two arrows if the target of one is the source of another. Except, that is, when the category contains only one object, in which case all arrows are composable.

A category with a single object is called a monoid. The combining operation is the composition of arrows and the unit is the identity arrow. 

This is a perfectly valid definition. In practice, however, we are often interested in monoids that are embedded in larger categories. In particular, in programming, we want to be able to define monoids inside the category of types and functions. 

However, in a category, rather than looking at individual elements, we prefer to define operations in bulk. So we start with an object $m$. A binary operation is a function of two arguments. Since elements of a product are pairs of elements, we can characterize a binary operation as an arrow from a product $m \times m$ to $m$:
\[ \mu \colon m \times m \to m \]
The unit element can be defined as an arrow from the terminal object $1$:
\[ \eta \colon 1 \to m \]

We can translate this description directly to Haskell by defining a \index{type class}class of types equipped with two methods, traditionally called \hask{mappend} and \hask{mempty}:
\begin{haskell}
class Monoid m where
  mappend :: (m, m) -> m
  mempty  :: () -> m
\end{haskell}

The two arrows $\mu$ and $\eta$ have to satisfy monoid laws but, again, we have to formulate them in bulk, without any recourse to elements.

To formulate the left unit law, we first create the product $1 \times m$. We then use $\eta$ to ``pick the unit element in $m$'' or, in terms of arrows, turn $1$ into $m$. Since we are operating on a product $1 \times m$, we have to lift the pair $\langle \eta, id_m \rangle$, which ensures that we ``do not touch'' the $m$. Finally we perform the ``multiplication'' using $\mu$. 

We want the result to be the same as the original element of $m$, but without mentioning elements. So we just use the left unitor $\lambda$ to go from $1 \times m$ to $m$ without ``stirring things up.''
\[
 \begin{tikzcd}
 1 \times m
 \arrow[rr, "\eta \times id_m"]
 \arrow[rrd, "\lambda"']
& & m \times m
 \arrow[d, "\mu"]
 \\
 && m
  \end{tikzcd}
\]
Here is the analogous law for the right unit:
\[
 \begin{tikzcd}
 m \times m
 \arrow[d, "\mu"]
 && m \times 1
 \arrow[ll, "id_m \times \eta"']
 \arrow[lld, "\rho"]
 \\
 m
 \end{tikzcd}
\]
To formulate the law of associativity, we have to start with a triple product and act on it in bulk. Here, $\alpha$ is the associator that rearranges the product without ``stirring things up.''
\[
 \begin{tikzcd}
 (m \times m) \times m 
 \arrow[rr, "\alpha"]
 \arrow[d, "\mu \times id"]
 &&
 m \times (m \times m)
 \arrow[d, "id \times \mu"]
 \\
 m \times m 
 \arrow[dr, "\mu"]
& & m \times m
 \arrow[dl, "\mu"']
 \\
&  m
 \end{tikzcd}
\]

Notice that we didn't have to assume a lot about the categorical product that we used with the objects $m$ and $1$. In particular we never had to use projections. This suggests that the above definition will work equally well for a tensor product in an arbitrary monoidal category. It doesn't even have to be symmetric. All we have to assume is that: there is a unit object, that the product is functorial, and that it satisfies the unit and associativity laws up to isomorphism.

Thus if we replace $\times$ with $\otimes$ and $1$ with $I$, we get a definition of a monoid in an arbitrary monoidal category. 

A \index{monoid}\emph{monoid} in a monoidal category is an object $m$ equipped with two morphisms:
\[ \mu \colon m \otimes m \to m \]
\[ \eta \colon I \to m \]
satisfying the unit and associativity laws:
\[
 \begin{tikzcd}
 1 \otimes m
 \arrow[rr, "\eta \otimes id_m"]
 \arrow[rrd, "\lambda"']
& & m \otimes m
 \arrow[d, "\mu"']
&& m \otimes 1
 \arrow[ll, "id_m \otimes \eta"']
 \arrow[lld, "\rho"]
 \\
 && m
  \end{tikzcd}
\]

\[
 \begin{tikzcd}
 (m \otimes m) \otimes m 
 \arrow[rr, "\alpha"]
 \arrow[d, "\mu \otimes id_m"]
 &&
 m \otimes (m \otimes m)
 \arrow[d, "id_m \otimes \mu"]
 \\
 m \otimes m 
 \arrow[dr, "\mu"]
& & m \otimes m
 \arrow[dl, "\mu"']
 \\
&  m
 \end{tikzcd}
\]
We used the functoriality of $\otimes$ to lift pairs of arrows, as in $\eta \otimes id_m$, $\mu \otimes id_m$, etc.

\end{document}
